idlnk{-}deq $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$product{-}deq(Id; (:Id $\times$ Id); id{-}deq; product{-}deq(Id; Id; id{-}deq; id{-}deq))